(0) Obligation:

Runtime Complexity TRS:
The TRS R consists of the following rules:

f(x, y, w, w, a) → g1(x, x, y, w)
f(x, y, w, a, a) → g1(y, x, x, w)
f(x, y, a, a, w) → g2(x, y, y, w)
f(x, y, a, w, w) → g2(y, y, x, w)
g1(x, x, y, a) → h(x, y)
g1(y, x, x, a) → h(x, y)
g2(x, y, y, a) → h(x, y)
g2(y, y, x, a) → h(x, y)
h(x, x) → x

Rewrite Strategy: INNERMOST

(1) CpxTrsToCdtProof (BOTH BOUNDS(ID, ID) transformation)

Converted CpxTRS to CDT

(2) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1, z2, z2, a) → g1(z0, z0, z1, z2)
f(z0, z1, z2, a, a) → g1(z1, z0, z0, z2)
f(z0, z1, a, a, z2) → g2(z0, z1, z1, z2)
f(z0, z1, a, z2, z2) → g2(z1, z1, z0, z2)
g1(z0, z0, z1, a) → h(z0, z1)
g1(z0, z1, z1, a) → h(z1, z0)
g2(z0, z1, z1, a) → h(z0, z1)
g2(z0, z0, z1, a) → h(z1, z0)
h(z0, z0) → z0
Tuples:

F(z0, z1, z2, z2, a) → c(G1(z0, z0, z1, z2))
F(z0, z1, z2, a, a) → c1(G1(z1, z0, z0, z2))
F(z0, z1, a, a, z2) → c2(G2(z0, z1, z1, z2))
F(z0, z1, a, z2, z2) → c3(G2(z1, z1, z0, z2))
G1(z0, z0, z1, a) → c4(H(z0, z1))
G1(z0, z1, z1, a) → c5(H(z1, z0))
G2(z0, z1, z1, a) → c6(H(z0, z1))
G2(z0, z0, z1, a) → c7(H(z1, z0))
S tuples:

F(z0, z1, z2, z2, a) → c(G1(z0, z0, z1, z2))
F(z0, z1, z2, a, a) → c1(G1(z1, z0, z0, z2))
F(z0, z1, a, a, z2) → c2(G2(z0, z1, z1, z2))
F(z0, z1, a, z2, z2) → c3(G2(z1, z1, z0, z2))
G1(z0, z0, z1, a) → c4(H(z0, z1))
G1(z0, z1, z1, a) → c5(H(z1, z0))
G2(z0, z1, z1, a) → c6(H(z0, z1))
G2(z0, z0, z1, a) → c7(H(z1, z0))
K tuples:none
Defined Rule Symbols:

f, g1, g2, h

Defined Pair Symbols:

F, G1, G2

Compound Symbols:

c, c1, c2, c3, c4, c5, c6, c7

(3) CdtLeafRemovalProof (BOTH BOUNDS(ID, ID) transformation)

Removed 8 trailing nodes:

G1(z0, z0, z1, a) → c4(H(z0, z1))
G1(z0, z1, z1, a) → c5(H(z1, z0))
F(z0, z1, a, a, z2) → c2(G2(z0, z1, z1, z2))
F(z0, z1, z2, a, a) → c1(G1(z1, z0, z0, z2))
G2(z0, z0, z1, a) → c7(H(z1, z0))
F(z0, z1, z2, z2, a) → c(G1(z0, z0, z1, z2))
F(z0, z1, a, z2, z2) → c3(G2(z1, z1, z0, z2))
G2(z0, z1, z1, a) → c6(H(z0, z1))

(4) Obligation:

Complexity Dependency Tuples Problem
Rules:

f(z0, z1, z2, z2, a) → g1(z0, z0, z1, z2)
f(z0, z1, z2, a, a) → g1(z1, z0, z0, z2)
f(z0, z1, a, a, z2) → g2(z0, z1, z1, z2)
f(z0, z1, a, z2, z2) → g2(z1, z1, z0, z2)
g1(z0, z0, z1, a) → h(z0, z1)
g1(z0, z1, z1, a) → h(z1, z0)
g2(z0, z1, z1, a) → h(z0, z1)
g2(z0, z0, z1, a) → h(z1, z0)
h(z0, z0) → z0
Tuples:none
S tuples:none
K tuples:none
Defined Rule Symbols:

f, g1, g2, h

Defined Pair Symbols:none

Compound Symbols:none

(5) SIsEmptyProof (EQUIVALENT transformation)

The set S is empty

(6) BOUNDS(O(1), O(1))